This paper introduces a formal metamodel for the\r\nspecification of security policies for workflows in online service\r\nsystems designed to be suitable for the modeling and analysis of\r\ncomplex business-related rules as well as traditional access\r\ncontrol. A translation of the model into a colored Petri net is\r\nshown and an example of policy for an online banking system is\r\ndescribed. By writing predicates for querying the resulting statespace\r\nof the Petri net, a connection between the formalized model\r\nand a higher-level description of the security policy can be made,\r\nindicating the feasibility of the intended method for validating\r\nsuch descriptions. Thanks to the independent nature among tasks\r\nrelated to different business services, represented by restrictions\r\nin the information flow within the metamodel, the state-space\r\nmay be fractioned for analysis, avoiding the state-space explosion\r\nproblem. Related existing models are discussed, pointing the gain\r\nin expressiveness of business rules and the analysis of insecure\r\nstate paths rather than simply insecure states in the proposed\r\nmodel. The successful representation and analysis of the policy\r\nfrom the example combined with reasonings for the general case\r\nattest the adequacy of the proposed approach for its intended\r\napplication.
Loading....